/**
 * Copyright (c) 2010 CWI Amsterdam and others. All rights reserved.
 * This program and the accompanying materials are made available
 * under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 * 
 * Contributors:
 *    CWI Amsterdam - initial API and implementation
 */
package nl.cwi.arne.generator.tools;

import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.util.List;

import nl.cwi.arne.Network;
import nl.cwi.arne.NetworkActivation;
import nl.cwi.arne.generator.NetworkActivationGenerator;
import nl.cwi.arne.generator.mcrl2.ArneMCRL2Translator;
import nl.cwi.arne.util.NetworkActivationBuffer;

import org.eclipse.core.runtime.IStatus;
import org.eclipse.core.runtime.NullProgressMonitor;
import org.eclipse.equinox.app.IApplicationContext;

/**
 * @author Christian Krause
 */
public class EquivalenceClassGeneratorTool extends AbstractGeneratorTool {

	/*
	 * (non-Javadoc)
	 * @see org.eclipse.equinox.app.IApplication#start(org.eclipse.equinox.app.IApplicationContext)
	 */
	@Override
	public Object start(IApplicationContext context) throws Exception {
		generate(context, true);
		return null;
	}
	
	
	private void generate(IApplicationContext context, boolean withZeroChanges) throws Exception {
		
		// Load the network:
		Network network = loadNetwork(context);
		network.setCheckEquivalence(true);
		network.setCheckModalFormula(false);
		network.setCheckStableRegions(false);
		network.getActivations().clear();

		// MCRL2 translator:
		ArneMCRL2Translator translator = new ArneMCRL2Translator();
		translator.setDeltaLabels(false);
		translator.setWithZeroChanges(withZeroChanges);
		translator.setStartFromZeroChange(true);
		translator.setVerboseLabels(true);
		
		// Activation generator:
		NetworkActivationGenerator generator = new NetworkActivationGenerator();
		generator.setMCRL2Options(getMCRL2Options());
		generator.setOutputStream(System.out);
		generator.setTranslator(translator);
		
		NetworkActivationBuffer buffer = new NetworkActivationBuffer(network);
		IStatus status = generator.generate(network, buffer, monitor);
		if (status.getSeverity()!=IStatus.OK) {
			System.err.println(status.getMessage());
			System.err.println(status.getException());
			return;
		}
		
		System.out.println("Verifying equivalence classes...");
		status = generator.getEquivalenceClasses().verify(new NullProgressMonitor());
		if (status.getSeverity()!=IStatus.OK) {
			System.err.println(status.getMessage());
			System.err.println(status.getException());
			return;
		} else {
			System.out.println("done.");
		}
		
		System.out.println("Saving class index...");
		String file = network.eResource().getURI().trimFileExtension().toFileString();
		save(generator, new File(file + ".classes"));
		
		System.out.println("Saving class LTS'...");
		generator.getEquivalenceClasses().saveLTSs(new File("/home/christian/Desktop/classes"));
		System.out.println("done.");
	}
	
	private void save(NetworkActivationGenerator generator, File file) throws IOException {
		BufferedWriter writer = new BufferedWriter(new FileWriter(file));
		writer.append(file.getName() + "\n");
		writer.append("\n--- GENERATED EQUIVALENCE CLASSES ---\n\n");
		int index = 0;
		for (List<NetworkActivation> clazz : generator.getEquivalenceClasses().values()) {
			writer.append("\n-- Class (" + (++index) + ") -- " + clazz.size() + " entries --\n");
			for (NetworkActivation activation : clazz) {
				writer.append(activation + "\n");
			}
		}
		writer.close();
	}
}
